package com.ecnu.codelearn.controller;

import com.ecnu.codelearn.common.HttpResult;
import com.ecnu.codelearn.software_analysis.FirstOrderLogic;
import com.ecnu.codelearn.software_analysis.ImpToFirstOrderLogicService;
import com.ecnu.codelearn.software_analysis.KripkeStructure;
import com.ecnu.codelearn.software_analysis.ProgramSegment;
import org.apache.commons.lang3.StringUtils;
import org.springframework.stereotype.Controller;
import org.springframework.web.bind.annotation.CrossOrigin;
import org.springframework.web.bind.annotation.GetMapping;
import org.springframework.web.bind.annotation.RequestParam;
import org.springframework.web.bind.annotation.ResponseBody;

import java.util.*;

/**
 * 软件分析与验证工具课程作业相关接口
 * @author caopeisheng
 */
@Controller
@CrossOrigin("*")
public class SoftwareAnalysisController {

    @GetMapping("/impToFirstOrderFormula")
    @ResponseBody
    public HttpResult ImpToFirstOrderFormula(String programInputString,
                                             @RequestParam(required = false) String initVarDefInput) {
        if (StringUtils.isEmpty(programInputString) || StringUtils.isEmpty(programInputString.trim())) {
            return HttpResult.error("programInputString输入不能为空");
        }
        programInputString = programInputString.trim();

        //处理驶入的初始变量赋值
        String initVarDefStr;
        if (StringUtils.isEmpty(initVarDefInput)) {
            initVarDefStr = "";
        } else {
            String[] splits = initVarDefInput.split(";");
            initVarDefStr = StringUtils.join(splits, " && ");
        }

        List<FirstOrderLogic> resultFirstOrder;
        try {
            ProgramSegment programSegment = ProgramSegment.build(programInputString);//获取程序标记
            ImpToFirstOrderLogicService impToFirstOrderLogicService = new ImpToFirstOrderLogicService();
            resultFirstOrder = impToFirstOrderLogicService.getResultFirstOrder(programSegment, initVarDefStr);//获取一阶逻辑公式
        } catch (Exception e) {
            return HttpResult.error(e.getMessage());
        }

        //封装返回数据
        Map<String, Object> resultMap = new HashMap<>();
        resultMap.put("resultFirstOrder", resultFirstOrder);

        List<KripkeStructure> kripkeStructureList;
        if (programInputString.contains("cobegin")) {
            kripkeStructureList = KripkeStructure.getConcurrentKSFromFirstOrderLogic(resultFirstOrder);
        } else {
            kripkeStructureList = KripkeStructure.getSerialKSFromFirstOrderLogic(resultFirstOrder);
        }
        resultMap.put("kripkeStructure", kripkeStructureList);

        return HttpResult.success(resultMap);
    }

    public static void main(String[] args) throws Exception {
        String programInputString = "cobegin while true do wait(turn==0);turn:=1;endwhile || while true do wait(turn==1);turn:=0;endwhile coend";
//        String programInputString = "x:=x+1;x:=x-1;skip;y:=y-1; while true do if x<y then wait(x>=y); endif endwhile";
//        String programInputString = "while true do wait(turn==0);turn:=1;endwhile ";
        String initVarDefStr = "turn:=1";

        //通过输入构建ProgramSegment
        ProgramSegment programSegment = ProgramSegment.build(programInputString);
        //通过ProgramSegment生成一阶逻辑公式
        ImpToFirstOrderLogicService impToFirstOrderLogicService = new ImpToFirstOrderLogicService();
        List<FirstOrderLogic> resultFirstOrder = impToFirstOrderLogicService.getResultFirstOrder(programSegment, initVarDefStr);

        resultFirstOrder.forEach(e -> System.out.println(e));

        //通过一阶逻辑公式，生成ks
        List<KripkeStructure> ks;
        if (programInputString.contains("cobegin")) {
            ks = KripkeStructure.getConcurrentKSFromFirstOrderLogic(resultFirstOrder);
        } else {
            ks = KripkeStructure.getSerialKSFromFirstOrderLogic(resultFirstOrder);
        }
        ks.forEach(e -> System.out.println(e));
    }


}
